# -*- coding: utf-8 -*-
"""
make_guards_4_3_from_attachment2.py
"""
import os, re
from pathlib import Path

HERE = Path(__file__).resolve().parent
SRC  = HERE / "modbus_full_stack.py"
OUT  = HERE / "guards_4_3_from_attachment2.horn"

def parse_supported_fc(text: str):
    m = re.search(r"SUPPORTED_FC\s*=\s*\{([^}]+)\}", text)
    if not m:
        return [1,2,3,4,5,6,15,16,22,23]
    raw = m.group(1)
    vals = []
    for tok in raw.split(","):
        t = tok.strip()
        if not t: 
            continue
        try:
            if t.lower().startswith("0x"):
                vals.append(int(t,16))
            else:
                vals.append(int(t))
        except:
            pass
    vals = sorted(set(vals))
    return vals

def parse_reg_cnt_max(text: str, default=2000):
    m = re.search(r"REG_CNT_MAX\s*=\s*(0x[0-9A-Fa-f]+|\d+)", text)
    if not m:
        return default
    lit = m.group(1)
    try:
        return int(lit,16) if lit.lower().startswith("0x") else int(lit)
    except:
        return default

def build_supported_fc_block(fcs):
    parts = [f"SupportedFC({x})." for x in fcs]
    lines = []
    if len(parts) >= 4:
        lines.append(" ".join(parts[:4]))
    else:
        lines.append(" ".join(parts))
        return "\n".join(lines)
    if len(parts) >= 8:
        lines.append(" ".join(parts[4:8]))
    elif len(parts) > 4:
        lines.append(" ".join(parts[4:]))
        return "\n".join(lines)
    if len(parts) > 8:
        lines.append(" ".join(parts[8:]))
    return "\n".join(lines)

def main():
    if not SRC.exists():
        raise SystemExit(f"[ERROR] 找不到附件2：{SRC}")
    text = SRC.read_text(encoding="utf-8", errors="ignore")
    fcs  = parse_supported_fc(text)
    regm = parse_reg_cnt_max(text, 2000)

    fc_block = build_supported_fc_block(fcs)

    horn = f"""% 4.3 守卫规则集合（以附件2 modbus_full_stack.py 为输入提取）
% Domains
.decl MBAP(tid:int, pid:int, len:int, uid:int)
.decl PDUlen(fc:int, plen:int)               % 原始PDU长度（不含UID）
.decl PDU01(start:int, qty:int)
.decl PDU02(start:int, qty:int)
.decl PDU03(start:int, qty:int)
.decl PDU04(start:int, qty:int)
.decl PDU05(addr:int, value:int)
.decl PDU06(addr:int, value:int)
.decl PDU0F(start:int, qty:int, bc:int, vbytes:int)
.decl PDU10(start:int, qty:int, bc:int, vbytes:int)
.decl PDU16(addr:int, andm:int, orm:int)
.decl PDU17(r_start:int, r_qty:int, w_start:int, w_qty:int, bc:int, vbytes:int)

.decl SupportedFC(fc:int)
.decl QtyOK_RCoils(qty:int)                   % 0x01/0x02 上限 2000
.decl QtyOK_RRegs(qty:int)                    % 0x03/0x04 上限 125
.decl QtyOK_WRegs(qty:int)                    % 0x10/0x17 写上限 123
.decl QtyOK_WCoils(qty:int)                   % 0x0F 写上限 1968
.decl BcOK_0F(bc:int, qty:int)
.decl BcOK_10(bc:int, qty:int)
.decl BcOK_17(bc:int, w_qty:int)
.decl AddrOK(start:int, qty:int)

% Outcomes (coarse-grained per server的异常映射)
.decl BadLen()                                 % 长度不合法
.decl BadProto()                               % 协议/功能不支持
.decl BadValue()                               % 值/字段不合法（ILLEGAL_DATA_VALUE）
.decl BadAddr()                                % 地址越界（ILLEGAL_DATA_ADDRESS）

% -------------------------------------------------------------------
% Constants (materialized as facts)
% -------------------------------------------------------------------
{fc_block}

QtyOK_RCoils(q) :- q >= 1, q =< 2000.
QtyOK_RRegs(q)  :- q >= 1, q =< 125.
QtyOK_WRegs(q)  :- q >= 1, q =< 123.
QtyOK_WCoils(q) :- q >= 1, q =< 1968.

BcOK_0F(bc,q)   :- bc = (q + 7) / 8.          % 整数除法，向下取整
BcOK_10(bc,q)   :- bc = 2*q.
BcOK_17(bc,q)   :- bc = 2*q.

AddrOK(s,q)     :- s + q =< {regm}.

% -------------------------------------------------------------------
% MBAP/传输层守卫
% -------------------------------------------------------------------

% R1: PID 必须为 0
BadProto()  :- MBAP(_, pid, _, _), pid != 0.

% R2: MBAP.len 不得为 0
BadLen()    :- MBAP(_, 0, 0, _).

% R3: PDU 长度必须 > 0  (len-1)
BadLen()    :- MBAP(_, 0, len, _), len - 1 =< 0.

% R4: PDU 不能为空
BadLen()    :- PDUlen(_, plen), plen < 1.

% R5: 功能码必须被支持
BadProto()  :- PDUlen(fc, _), not SupportedFC(fc).

% -------------------------------------------------------------------
% FC 不同形状的“最小长度”守卫（短PDU）
% -------------------------------------------------------------------

% 0x01..0x04 统一：至少 5 字节
BadValue()  :- PDUlen(1, plen),  plen < 5.
BadValue()  :- PDUlen(2, plen),  plen < 5.
BadValue()  :- PDUlen(3, plen),  plen < 5.
BadValue()  :- PDUlen(4, plen),  plen < 5.

% 0x05/0x06：至少 5 字节
BadValue()  :- PDUlen(5, plen),  plen < 5.
BadValue()  :- PDUlen(6, plen),  plen < 5.

% 0x0F：至少 6 字节（含 ByteCount）
BadValue()  :- PDUlen(15, plen), plen < 6.

% 0x10：至少 6 字节（含 ByteCount）
BadValue()  :- PDUlen(16, plen), plen < 6.

% 0x16：至少 7 字节（addr+and+or）
BadValue()  :- PDUlen(22, plen), plen < 7.

% 0x17：至少 11 字节（读写参数+bc）
BadValue()  :- PDUlen(23, plen), plen < 11.

% -------------------------------------------------------------------
% FC=0x01 Read Coils
% -------------------------------------------------------------------
BadValue()  :- PDU01(_, qty), not QtyOK_RCoils(qty).
BadAddr()   :- PDU01(start, qty), QtyOK_RCoils(qty), not AddrOK(start, qty).

% -------------------------------------------------------------------
% FC=0x02 Read Discrete Inputs
% -------------------------------------------------------------------
BadValue()  :- PDU02(_, qty), not QtyOK_RCoils(qty).
BadAddr()   :- PDU02(start, qty), QtyOK_RCoils(qty), not AddrOK(start, qty).

% -------------------------------------------------------------------
% FC=0x03 Read Holding Registers
% -------------------------------------------------------------------
BadValue()  :- PDU03(_, qty), not QtyOK_RRegs(qty).
BadAddr()   :- PDU03(start, qty), QtyOK_RRegs(qty), not AddrOK(start, qty).

% -------------------------------------------------------------------
% FC=0x04 Read Input Registers
% -------------------------------------------------------------------
BadValue()  :- PDU04(_, qty), not QtyOK_RRegs(qty).
BadAddr()   :- PDU04(start, qty), QtyOK_RRegs(qty), not AddrOK(start, qty).

% -------------------------------------------------------------------
% FC=0x05 Write Single Coil
%   注：实现接受任意 value（仅将 0xFF00 视为 True），因此无 Value 守卫；地址越界仍然触发 BadAddr
% -------------------------------------------------------------------
BadAddr()   :- PDU05(addr, _), not AddrOK(addr, 1).

% -------------------------------------------------------------------
% FC=0x06 Write Single Register
% -------------------------------------------------------------------
BadAddr()   :- PDU06(addr, _), not AddrOK(addr, 1).

% -------------------------------------------------------------------
% FC=0x0F Write Multiple Coils
% -------------------------------------------------------------------
BadValue()  :- PDU0F(_, qty, _, _), not QtyOK_WCoils(qty).
BadAddr()   :- PDU0F(start, qty, _, _), QtyOK_WCoils(qty), not AddrOK(start, qty).
BadValue()  :- PDU0F(_, qty, bc, _), QtyOK_WCoils(qty), not BcOK_0F(bc, qty).

% -------------------------------------------------------------------
% FC=0x10 Write Multiple Registers
% -------------------------------------------------------------------
BadValue()  :- PDU10(_, qty, _, _), not QtyOK_WRegs(qty).
BadValue()  :- PDU10(_, qty, bc, _), QtyOK_WRegs(qty), not BcOK_10(bc, qty).
BadAddr()   :- PDU10(start, qty, bc, _), QtyOK_WRegs(qty), BcOK_10(bc, qty), not AddrOK(start, qty).
BadValue()  :- PDU10(_, qty, bc, vbytes), QtyOK_WRegs(qty), BcOK_10(bc, qty), vbytes < 2*qty.

% -------------------------------------------------------------------
% FC=0x16 Mask Write Register
% -------------------------------------------------------------------
BadAddr()   :- PDU16(addr, _, _), not AddrOK(addr, 1).

% -------------------------------------------------------------------
% FC=0x17 Read/Write Multiple Registers（简化版）
% -------------------------------------------------------------------
BadValue()  :- PDU17(_, r_qty, _, _, _, _), not QtyOK_RRegs(r_qty).
BadValue()  :- PDU17(_, _, _, w_qty, _, _), not QtyOK_WRegs(w_qty).
BadValue()  :- PDU17(_, _, _, w_qty, bc, _), QtyOK_WRegs(w_qty), not BcOK_17(bc, w_qty).
BadAddr()   :- PDU17(r_start, r_qty, _, _, _, _), QtyOK_RRegs(r_qty), not AddrOK(r_start, r_qty).
BadAddr()   :- PDU17(_, _, w_start, w_qty, bc, _), QtyOK_WRegs(w_qty), BcOK_17(bc, w_qty), not AddrOK(w_start, w_qty).
BadValue()  :- PDU17(_, _, _, w_qty, bc, vbytes), QtyOK_WRegs(w_qty), BcOK_17(bc, w_qty), vbytes < 2*w_qty.

% -------------------------------------------------------------------
% 说明：服务器在 BadProto/BadLen/BadValue/BadAddr 时的响应映射由实现决定；
% 该集合仅覆盖“可达的守卫条件”，与具体异常码绑定见实现。
"""
    OUT.write_text(horn, encoding="utf-8")
    print(f"[OK] 写出：{OUT}")

if __name__ == "__main__":
    main()
